Left Termination of the query pattern
reach(g,g,g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 88 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 99 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 26 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 PiDPToQDPProof (⇒, 0 ms)
        ↳37 QDP
        ↳38 QDPOrderProof (⇔, 97 ms)
        ↳39 QDP
        ↳40 DependencyGraphProof (⇔, 0 ms)
        ↳41 TRUE

(0) Obligation:

Clauses:

reach(X, Y, E, L) :- member(.(X, .(Y, [])), E).
reach(X, Z, E, L) :- ','(member1(.(X, .(Y, [])), E), ','(member(Y, L), ','(delete(Y, L, V1), reach(Y, Z, E, V1)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).
delete(X, .(X, Y), Y).
delete(X, .(H, T1), .(H, T2)) :- delete(X, T1, T2).

Query: reach(g,g,g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

memberA(X1, X2, .(X3, X4)) :- memberA(X1, X2, X4).
member1B(X1, X2, .(X3, X4)) :- member1B(X1, X2, X4).
memberC(X1, .(X2, X3)) :- memberC(X1, X3).
deleteE(X1, .(X2, X3), .(X2, X4)) :- deleteE(X1, X3, X4).
reachD(X1, X2, .(X3, X4), X5) :- memberA(X1, X2, X4).
reachD(X1, X2, X3, X4) :- member1B(X1, X5, X3).
reachD(X1, X2, X3, X4) :- ','(member1cB(X1, X5, X3), memberC(X5, X4)).
reachD(X1, X2, X3, X4) :- ','(member1cB(X1, X5, X3), ','(membercC(X5, X4), deleteE(X5, X4, X6))).
reachD(X1, X2, X3, X4) :- ','(member1cB(X1, X5, X3), ','(membercC(X5, X4), ','(deletecE(X5, X4, X6), reachD(X5, X2, X3, X6)))).

Clauses:

membercA(X1, X2, .(.(X1, .(X2, [])), X3)).
membercA(X1, X2, .(X3, X4)) :- membercA(X1, X2, X4).
member1cB(X1, X2, .(.(X1, .(X2, [])), X3)).
member1cB(X1, X2, .(X3, X4)) :- member1cB(X1, X2, X4).
membercC(X1, .(X1, X2)).
membercC(X1, .(X2, X3)) :- membercC(X1, X3).
reachcD(X1, X2, .(.(X1, .(X2, [])), X3), X4).
reachcD(X1, X2, .(X3, X4), X5) :- membercA(X1, X2, X4).
reachcD(X1, X2, X3, X4) :- ','(member1cB(X1, X5, X3), ','(membercC(X5, X4), ','(deletecE(X5, X4, X6), reachcD(X5, X2, X3, X6)))).
deletecE(X1, .(X1, X2), X2).
deletecE(X1, .(X2, X3), .(X2, X4)) :- deletecE(X1, X3, X4).

Afs:

reachD(x1, x2, x3, x4)  =  reachD(x1, x2, x3, x4)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
reachD_in: (b,b,b,b)
memberA_in: (b,b,b)
member1B_in: (b,f,b)
member1cB_in: (b,f,b)
memberC_in: (b,b)
membercC_in: (b,b)
deleteE_in: (b,b,f)
deletecE_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → U5_GGGG(X1, X2, X3, X4, X5, memberA_in_ggg(X1, X2, X4))
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → MEMBERA_IN_GGG(X1, X2, X4)
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → U1_GGG(X1, X2, X3, X4, memberA_in_ggg(X1, X2, X4))
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U6_GGGG(X1, X2, X3, X4, member1B_in_gag(X1, X5, X3))
REACHD_IN_GGGG(X1, X2, X3, X4) → MEMBER1B_IN_GAG(X1, X5, X3)
MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, member1B_in_gag(X1, X2, X4))
MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, member1cB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U8_GGGG(X1, X2, X3, X4, memberC_in_gg(X5, X4))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → MEMBERC_IN_GG(X5, X4)
MEMBERC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, memberC_in_gg(X1, X3))
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U10_GGGG(X1, X2, X3, X4, deleteE_in_gga(X5, X4, X6))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → DELETEE_IN_GGA(X5, X4, X6)
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → U4_GGA(X1, X2, X3, X4, deleteE_in_gga(X1, X3, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → U12_GGGG(X1, X2, X3, X4, reachD_in_gggg(X5, X2, X3, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
reachD_in_gggg(x1, x2, x3, x4)  =  reachD_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
memberA_in_ggg(x1, x2, x3)  =  memberA_in_ggg(x1, x2, x3)
member1B_in_gag(x1, x2, x3)  =  member1B_in_gag(x1, x3)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
memberC_in_gg(x1, x2)  =  memberC_in_gg(x1, x2)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deleteE_in_gga(x1, x2, x3)  =  deleteE_in_gga(x1, x2)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
REACHD_IN_GGGG(x1, x2, x3, x4)  =  REACHD_IN_GGGG(x1, x2, x3, x4)
U5_GGGG(x1, x2, x3, x4, x5, x6)  =  U5_GGGG(x1, x2, x3, x4, x5, x6)
MEMBERA_IN_GGG(x1, x2, x3)  =  MEMBERA_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5)  =  U1_GGG(x1, x2, x3, x4, x5)
U6_GGGG(x1, x2, x3, x4, x5)  =  U6_GGGG(x1, x2, x3, x4, x5)
MEMBER1B_IN_GAG(x1, x2, x3)  =  MEMBER1B_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x3, x4, x5)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x1, x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5)  =  U8_GGGG(x1, x2, x3, x4, x5)
MEMBERC_IN_GG(x1, x2)  =  MEMBERC_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U9_GGGG(x1, x2, x3, x4, x5, x6)  =  U9_GGGG(x1, x2, x3, x4, x5, x6)
U10_GGGG(x1, x2, x3, x4, x5)  =  U10_GGGG(x1, x2, x3, x4, x5)
DELETEE_IN_GGA(x1, x2, x3)  =  DELETEE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U11_GGGG(x1, x2, x3, x4, x5, x6)  =  U11_GGGG(x1, x2, x3, x4, x5, x6)
U12_GGGG(x1, x2, x3, x4, x5)  =  U12_GGGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → U5_GGGG(X1, X2, X3, X4, X5, memberA_in_ggg(X1, X2, X4))
REACHD_IN_GGGG(X1, X2, .(X3, X4), X5) → MEMBERA_IN_GGG(X1, X2, X4)
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → U1_GGG(X1, X2, X3, X4, memberA_in_ggg(X1, X2, X4))
MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U6_GGGG(X1, X2, X3, X4, member1B_in_gag(X1, X5, X3))
REACHD_IN_GGGG(X1, X2, X3, X4) → MEMBER1B_IN_GAG(X1, X5, X3)
MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, member1B_in_gag(X1, X2, X4))
MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X2, X4)
REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, member1cB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U8_GGGG(X1, X2, X3, X4, memberC_in_gg(X5, X4))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → MEMBERC_IN_GG(X5, X4)
MEMBERC_IN_GG(X1, .(X2, X3)) → U3_GG(X1, X2, X3, memberC_in_gg(X1, X3))
MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U10_GGGG(X1, X2, X3, X4, deleteE_in_gga(X5, X4, X6))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → DELETEE_IN_GGA(X5, X4, X6)
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → U4_GGA(X1, X2, X3, X4, deleteE_in_gga(X1, X3, X4))
DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → U12_GGGG(X1, X2, X3, X4, reachD_in_gggg(X5, X2, X3, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
reachD_in_gggg(x1, x2, x3, x4)  =  reachD_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
memberA_in_ggg(x1, x2, x3)  =  memberA_in_ggg(x1, x2, x3)
member1B_in_gag(x1, x2, x3)  =  member1B_in_gag(x1, x3)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
memberC_in_gg(x1, x2)  =  memberC_in_gg(x1, x2)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deleteE_in_gga(x1, x2, x3)  =  deleteE_in_gga(x1, x2)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
REACHD_IN_GGGG(x1, x2, x3, x4)  =  REACHD_IN_GGGG(x1, x2, x3, x4)
U5_GGGG(x1, x2, x3, x4, x5, x6)  =  U5_GGGG(x1, x2, x3, x4, x5, x6)
MEMBERA_IN_GGG(x1, x2, x3)  =  MEMBERA_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5)  =  U1_GGG(x1, x2, x3, x4, x5)
U6_GGGG(x1, x2, x3, x4, x5)  =  U6_GGGG(x1, x2, x3, x4, x5)
MEMBER1B_IN_GAG(x1, x2, x3)  =  MEMBER1B_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x3, x4, x5)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x1, x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5)  =  U8_GGGG(x1, x2, x3, x4, x5)
MEMBERC_IN_GG(x1, x2)  =  MEMBERC_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U9_GGGG(x1, x2, x3, x4, x5, x6)  =  U9_GGGG(x1, x2, x3, x4, x5, x6)
U10_GGGG(x1, x2, x3, x4, x5)  =  U10_GGGG(x1, x2, x3, x4, x5)
DELETEE_IN_GGA(x1, x2, x3)  =  DELETEE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U11_GGGG(x1, x2, x3, x4, x5, x6)  =  U11_GGGG(x1, x2, x3, x4, x5, x6)
U12_GGGG(x1, x2, x3, x4, x5)  =  U12_GGGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 13 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
DELETEE_IN_GGA(x1, x2, x3)  =  DELETEE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_GGA(X1, .(X2, X3), .(X2, X4)) → DELETEE_IN_GGA(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
DELETEE_IN_GGA(x1, x2, x3)  =  DELETEE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEE_IN_GGA(X1, .(X2, X3)) → DELETEE_IN_GGA(X1, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELETEE_IN_GGA(X1, .(X2, X3)) → DELETEE_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
MEMBERC_IN_GG(x1, x2)  =  MEMBERC_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBERC_IN_GG(X1, .(X2, X3)) → MEMBERC_IN_GG(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X2, X4)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
MEMBER1B_IN_GAG(x1, x2, x3)  =  MEMBER1B_IN_GAG(x1, x3)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1B_IN_GAG(X1, X2, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X2, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
MEMBER1B_IN_GAG(x1, x2, x3)  =  MEMBER1B_IN_GAG(x1, x3)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBER1B_IN_GAG(X1, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBER1B_IN_GAG(X1, .(X3, X4)) → MEMBER1B_IN_GAG(X1, X4)
    The graph contains the following edges 1 >= 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
MEMBERA_IN_GGG(x1, x2, x3)  =  MEMBERA_IN_GGG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBERA_IN_GGG(X1, X2, .(X3, X4)) → MEMBERA_IN_GGG(X1, X2, X4)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, member1cB_in_gag(X1, X5, X3))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4, X6))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)

The TRS R consists of the following rules:

member1cB_in_gag(X1, X2, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, X2, .(X3, X4)) → U15_gag(X1, X2, X3, X4, member1cB_in_gag(X1, X2, X4))
U15_gag(X1, X2, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2), X2) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3), .(X2, X4)) → U22_gga(X1, X2, X3, X4, deletecE_in_gga(X1, X3, X4))
U22_gga(X1, X2, X3, X4, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member1cB_in_gag(x1, x2, x3)  =  member1cB_in_gag(x1, x3)
[]  =  []
member1cB_out_gag(x1, x2, x3)  =  member1cB_out_gag(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5)  =  U15_gag(x1, x3, x4, x5)
membercC_in_gg(x1, x2)  =  membercC_in_gg(x1, x2)
membercC_out_gg(x1, x2)  =  membercC_out_gg(x1, x2)
U16_gg(x1, x2, x3, x4)  =  U16_gg(x1, x2, x3, x4)
deletecE_in_gga(x1, x2, x3)  =  deletecE_in_gga(x1, x2)
deletecE_out_gga(x1, x2, x3)  =  deletecE_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4, x5)  =  U22_gga(x1, x2, x3, x5)
REACHD_IN_GGGG(x1, x2, x3, x4)  =  REACHD_IN_GGGG(x1, x2, x3, x4)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x1, x2, x3, x4, x5)
U9_GGGG(x1, x2, x3, x4, x5, x6)  =  U9_GGGG(x1, x2, x3, x4, x5, x6)
U11_GGGG(x1, x2, x3, x4, x5, x6)  =  U11_GGGG(x1, x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains

(36) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, member1cB_in_gag(X1, X3))
U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)

The TRS R consists of the following rules:

member1cB_in_gag(X1, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, .(X3, X4)) → U15_gag(X1, X3, X4, member1cB_in_gag(X1, X4))
U15_gag(X1, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The set Q consists of the following terms:

member1cB_in_gag(x0, x1)
U15_gag(x0, x1, x2, x3)
membercC_in_gg(x0, x1)
U16_gg(x0, x1, x2, x3)
deletecE_in_gga(x0, x1)
U22_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U7_GGGG(X1, X2, X3, X4, member1cB_out_gag(X1, X5, X3)) → U9_GGGG(X1, X2, X3, X4, X5, membercC_in_gg(X5, X4))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(REACHD_IN_GGGG(x1, x2, x3, x4)) = 1 + x4   
POL(U11_GGGG(x1, x2, x3, x4, x5, x6)) = x6   
POL(U15_gag(x1, x2, x3, x4)) = 0   
POL(U16_gg(x1, x2, x3, x4)) = 0   
POL(U22_gga(x1, x2, x3, x4)) = 1 + x4   
POL(U7_GGGG(x1, x2, x3, x4, x5)) = 1 + x4   
POL(U9_GGGG(x1, x2, x3, x4, x5, x6)) = x4   
POL([]) = 0   
POL(deletecE_in_gga(x1, x2)) = x2   
POL(deletecE_out_gga(x1, x2, x3)) = 1 + x3   
POL(member1cB_in_gag(x1, x2)) = 0   
POL(member1cB_out_gag(x1, x2, x3)) = 0   
POL(membercC_in_gg(x1, x2)) = 0   
POL(membercC_out_gg(x1, x2)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REACHD_IN_GGGG(X1, X2, X3, X4) → U7_GGGG(X1, X2, X3, X4, member1cB_in_gag(X1, X3))
U9_GGGG(X1, X2, X3, X4, X5, membercC_out_gg(X5, X4)) → U11_GGGG(X1, X2, X3, X4, X5, deletecE_in_gga(X5, X4))
U11_GGGG(X1, X2, X3, X4, X5, deletecE_out_gga(X5, X4, X6)) → REACHD_IN_GGGG(X5, X2, X3, X6)

The TRS R consists of the following rules:

member1cB_in_gag(X1, .(.(X1, .(X2, [])), X3)) → member1cB_out_gag(X1, X2, .(.(X1, .(X2, [])), X3))
member1cB_in_gag(X1, .(X3, X4)) → U15_gag(X1, X3, X4, member1cB_in_gag(X1, X4))
U15_gag(X1, X3, X4, member1cB_out_gag(X1, X2, X4)) → member1cB_out_gag(X1, X2, .(X3, X4))
membercC_in_gg(X1, .(X1, X2)) → membercC_out_gg(X1, .(X1, X2))
membercC_in_gg(X1, .(X2, X3)) → U16_gg(X1, X2, X3, membercC_in_gg(X1, X3))
U16_gg(X1, X2, X3, membercC_out_gg(X1, X3)) → membercC_out_gg(X1, .(X2, X3))
deletecE_in_gga(X1, .(X1, X2)) → deletecE_out_gga(X1, .(X1, X2), X2)
deletecE_in_gga(X1, .(X2, X3)) → U22_gga(X1, X2, X3, deletecE_in_gga(X1, X3))
U22_gga(X1, X2, X3, deletecE_out_gga(X1, X3, X4)) → deletecE_out_gga(X1, .(X2, X3), .(X2, X4))

The set Q consists of the following terms:

member1cB_in_gag(x0, x1)
U15_gag(x0, x1, x2, x3)
membercC_in_gg(x0, x1)
U16_gg(x0, x1, x2, x3)
deletecE_in_gga(x0, x1)
U22_gga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(40) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(41) TRUE